<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Inline</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Background">\documentclass{article}

\usepackage{agda}

\begin{document}

Assume that we are given a type
%
</a><a id="97" class="Markup">\begin{code}[inline=False,hide=true]</a>
  <a id="136" class="Keyword">module</a> <a id="143" href="Inline.html" class="Module">_</a> <a id="145" class="Symbol">(</a>
<a id="147" class="Markup">\end{code}</a><a id="157" class="Background">
</a><a id="158" class="Markup">\begin{code}[hide,inline,hide=false]</a>
    <a id="199" href="Inline.html#199" class="Bound">A</a> <a id="201" class="Symbol">:</a> <a id="203" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="207" class="Markup">\end{code}</a><a id="217" class="Background">
</a><a id="218" class="Markup">\begin{code}[hide=false,hide=True]</a>
    <a id="257" class="Symbol">)</a> <a id="259" class="Symbol">(</a>
<a id="261" class="Markup">\end{code}</a><a id="271" class="Background">
%
,
and that a function
%
</a><a id="298" class="Markup">\begin{code}[inline*]</a>
    <a id="324" href="Inline.html#324" class="Bound">F</a> <a id="326" class="Symbol">:</a> <a id="328" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="332" class="Symbol">→</a> <a id="334" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="338" class="Symbol">→</a> <a id="340" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="344" class="Symbol">→</a> <a id="346" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="350" class="Markup">\end{code}</a><a id="360" class="Background">
</a><a id="361" class="Markup">\begin{code}[hide]</a>
    <a id="384" class="Symbol">)</a> <a id="386" class="Keyword">where</a>
<a id="392" class="Markup">\end{code}</a><a id="402" class="Background">
%
is also given.

\end{document}
</a></pre></body></html>